ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-trans(x)  ecl-trans-tuple{i:l}(ds;da) 

latex

Definitions	x:A. B(x), t  T, ecl-trans(x), p  q, isl(x), if b t else f fi, outl(x), , x,y. t(x;y), x,y,z,w. t(x;y;z;w), AB, A, P  Q, False, true, false, x,y,z. t(x;y;z), x. t(x), x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), Prop, x(s)
Lemmas	ecl ind wf, ecl-trans-tuple wf, ecl-base-tuple wf, decl-state wf, ma-valtype wf, bool wf, combine-ecl-tuples wf, bor wf, band wf, lt int wf, le wf, nat wf, combine-ecl-tuples2 wf, ifthenelse wf, eq int wf, bfalse wf, reset-ecl-tuple wf, add-ecl-act wf, ecl-add-throw wf, ecl-add-catch wf, ecl wf, fpf wf, Knd wf, Id wf